Prove the sharp N+4 state law - #3

What changed

This closes the remaining one-state gap in the lazy-point switch bound.

The new theorem

GeneralN.state_law_N_add_four : StateLawNAddFour

proves that every run on an N-switch layout visits at most N + 4 distinct restricted tongue vectors, including arbitrary starts. Combined with the existing symbolic lower bound and finite-state ceiling, the repository now proves

f(N) = min(2^N, N + 4)  for N ≥ 1.

Proof structure

BoundaryResidualSharpening.lean had reduced the arbitrary-start lift to four concrete residual geometries. This PR eliminates all four:

• strict stem approaches cannot first-write their own boundary switch;
• approach-writing the previous flip action is absorbed by the reserved-coordinate N+3 charge;
• a second manufacture starting at the boundary stem cannot productively first-write that switch;
• both occurrence-saving support-damage cases are eliminated using either the canonical self-link/two-phase history or a noncanonical double-duplicate history substitution that makes room for the time-zero vector without increasing the history budget.

StateLawNAddFourSharp.lean assembles these eliminations, proves ProductiveInitialBoundaryNAddFour, and invokes the exact arbitrary-start wrapper.

Repository updates

• registers the five new Lean libraries in lakefile.toml;
• audits the sharp theorem in StateLawAxiomAudit.lean;
• updates the theory documentation from the N+5 frontier to the exact law;
• fixes the permanent GitHub Actions check so it audits state_law_N_add_four rather than the stale historical stateLaw theorem.

Validation

An independent GitHub Actions verification built the complete project successfully:

• lake build: 525 jobs completed successfully;
• all 262 Lean libraries checked with Lean 4.32.2;
• StateLawAxiomAudit reports only [propext, Classical.choice, Quot.sound] for GeneralN.state_law_N_add_four;
• no sorryAx was present.